Nuprl Lemma : rem_bounds_4
13,42
postcript
pdf
a
:
,
n
:{...-1}. (0
(
a
rem
n
)) & ((
a
rem
n
) < (-
n
))
latex
Up
int
2
,
int
2
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
False
,
P
Q
,
A
,
A
B
,
i
j
,
{...
i
}
,
Lemmas
nat
wf
,
int
lower
wf
origin
a:
, n:{...-1}. (0 
(a rem n)) & ((a rem n) < (-n)) a:, n:{...-1}. (0 (a rem n)) & ((a rem n) < (-n)) 
Tx:A. B(x)
Q
A B
j